Nuprl Lemma : int_hgrp_el_wf
13,42
postcript
pdf
n
:
. zhgrp(
n
)
|(<
+>
hgrp)|
latex
Up
groups
1
Definitions of Statement
zhgrp(
n
)
Definitions
zhgrp(
n
)
,
t
T
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
nat
wf
,
nat
inc
origin
n:
. zhgrp(n) 
|(<
+>
hgrp)| n:. zhgrp(n) |(<+>hgrp)| Tx:A. B(x)
T